| 1: | a__f(X) | → cons(mark(X),f(g(X))) | |
| 2: | a__g(0) | → s(0) | |
| 3: | a__g(s(X)) | → s(s(a__g(mark(X)))) | |
| 4: | a__sel(0,cons(X,Y)) | → mark(X) | |
| 5: | a__sel(s(X),cons(Y,Z)) | → a__sel(mark(X),mark(Z)) | |
| 6: | mark(f(X)) | → a__f(mark(X)) | |
| 7: | mark(g(X)) | → a__g(mark(X)) | |
| 8: | mark(sel(X1,X2)) | → a__sel(mark(X1),mark(X2)) | |
| 9: | mark(cons(X1,X2)) | → cons(mark(X1),X2) | |
| 10: | mark(0) | → 0 | |
| 11: | mark(s(X)) | → s(mark(X)) | |
| 12: | a__f(X) | → f(X) | |
| 13: | a__g(X) | → g(X) | |
| 14: | a__sel(X1,X2) | → sel(X1,X2) | |
| 15: | A__F(X) | → MARK(X) | |
| 16: | A__G(s(X)) | → A__G(mark(X)) | |
| 17: | A__G(s(X)) | → MARK(X) | |
| 18: | A__SEL(0,cons(X,Y)) | → MARK(X) | |
| 19: | A__SEL(s(X),cons(Y,Z)) | → A__SEL(mark(X),mark(Z)) | |
| 20: | A__SEL(s(X),cons(Y,Z)) | → MARK(X) | |
| 21: | A__SEL(s(X),cons(Y,Z)) | → MARK(Z) | |
| 22: | MARK(f(X)) | → A__F(mark(X)) | |
| 23: | MARK(f(X)) | → MARK(X) | |
| 24: | MARK(g(X)) | → A__G(mark(X)) | |
| 25: | MARK(g(X)) | → MARK(X) | |
| 26: | MARK(sel(X1,X2)) | → A__SEL(mark(X1),mark(X2)) | |
| 27: | MARK(sel(X1,X2)) | → MARK(X1) | |
| 28: | MARK(sel(X1,X2)) | → MARK(X2) | |
| 29: | MARK(cons(X1,X2)) | → MARK(X1) | |
| 30: | MARK(s(X)) | → MARK(X) | |